Nuprl Lemma : es-next-bool-assign_wf 11,40
es:ES, v:, x:Id, e:{e:E| @loc(e)(x:)} , e':{e':E| e loc e'  & (x after e') = v} .
next event in [e,e'] after which x = v  E 
latex

Definitionsnext event in [e,bound] after which x = b, P  Q, A c B, t  T, e loc e' , P & Q, x:A. B(x), P  Q, , @i(x:T)
Lemmasbool-deq wf, es-next-assign wf, event system wf, Id wf, es-loc wf, es-dtype wf, es-E wf, bool wf, es-vartype wf, es-le-loc, es-after wf, es-locl wf

origin